M1, M2:msga{i:l}. ma-sub{i:l}(M1; M2)  {i'} 

latex

Definitions	P  Q, x:A. B(x), Top, Knd, IdLnk, t.1, Id, Void, rcv(l,tg), t.2, f(x)?z, Type, type List, x. t(x), t  T, x.A(x), State(ds), x:AB(x), x:A  B(x), , , a:A fp B(a), P & Q, FinProbSpace, f  g, product-deq(A;B;a;b), IdLnkDeq, KindDeq, IdDeq, , A c B, Valtype(da;k), MsgA, M1  M2
Lemmas	msga wf, Id wf, id-deq wf, Knd wf, Kind-deq wf, idlnk-deq wf, product-deq wf, fpf-sub wf, finite-prob-space wf, fpf-trivial-subtype-top, subtype-fpf2, IdLnk wf, ma-state wf, bool wf, rationals wf, subtype rel product, pi1 wf, top wf, subtype rel dep function, subtype rel self, subtype rel function, rcv wf, pi2 wf, fpf-cap wf, subtype rel list, subtype-fpf-cap-void, subtype-fpf-cap-top